<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>TheoremStmtGroup</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="TheoremStmtGroup";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/tl/TlConstants.html" title="class in mmj.tl"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/tl/TheoremStmtGroup.html" target="_top">Frames</a></li>
<li><a href="TheoremStmtGroup.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.tl</div>
<h2 title="Class TheoremStmtGroup" class="title">Class TheoremStmtGroup</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.tl.TheoremStmtGroup</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">TheoremStmtGroup</span>
extends java.lang.Object</pre>
<div class="block">TheoremStmtGroup represents the contents of a MMTTheoremFile as well as state
 variables pertaining to work performed loading the theorem into the
 LogicalSystem.
 <p>
 Note: TheoremStmtGroup refers to the fact that a MMTTheoremFile consists of a
 group of Metamath .mm statements.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.util.Comparator&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#NBR_LOG_HYP_SEQ">NBR_LOG_HYP_SEQ</a></strong></code>
<div class="block">NBR_LOG_HYP_SEQ sequences by number of LogHyps and Seq.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.util.Comparator&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#SEQ">SEQ</a></strong></code>
<div class="block">SEQ sequences by TheoremStmtGroup.theorem.getSeq().</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#TheoremStmtGroup(mmj.tl.MMTTheoremFile, mmj.lang.LogicalSystem, mmj.lang.Messages, mmj.tl.TlPreferences)">TheoremStmtGroup</a></strong>(<a href="../../mmj/tl/MMTTheoremFile.html" title="class in mmj.tl">MMTTheoremFile</a>&nbsp;mmtTheoremFile,
                <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                <a href="../../mmj/tl/TlPreferences.html" title="class in mmj.tl">TlPreferences</a>&nbsp;tlPreferences)</code>
<div class="block">Constructor for TheoremStmtGroup.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#compareTo(java.lang.Object)">compareTo</a></strong>(java.lang.Object&nbsp;obj)</code>
<div class="block">Compares TheoremStmtGroup object based on the label.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#equals(java.lang.Object)">equals</a></strong>(java.lang.Object&nbsp;obj)</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getAssignedLogHypSeq()">getAssignedLogHypSeq</a></strong>()</code>
<div class="block">Returns the assigned sequence number array for new Logical Hypotheses.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getAssignedTheoremSeq()">getAssignedTheoremSeq</a></strong>()</code>
<div class="block">Returns the assigned sequence number for a new Theorem.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getInsertSectionNbr()">getInsertSectionNbr</a></strong>()</code>
<div class="block">Gets the BookManager insertSectionNbr for the theorem.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getIsTheoremNew()">getIsTheoremNew</a></strong>()</code>
<div class="block">Gets the isTheoremNew flag.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getLogHypArray()">getLogHypArray</a></strong>()</code>
<div class="block">Gets the LogHyp array which may contain nulls if the Theorem is new and
 has not yet been stored in the Logical System.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getSourceFileName()">getSourceFileName</a></strong>()</code>
<div class="block">Returns the MMTTheoremFile absolute pathname.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getTheorem()">getTheorem</a></strong>()</code>
<div class="block">Gets the Theorem object or null if the theorem is new and has not yet
 been stored in the Logical System.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getTheoremLabel()">getTheoremLabel</a></strong>()</code>
<div class="block">Gets the theorem label.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getWasLogHypAppendedArray()">getWasLogHypAppendedArray</a></strong>()</code>
<div class="block">Gets the wasLogHypAppended flag array.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getWasLogHypInsertedArray()">getWasLogHypInsertedArray</a></strong>()</code>
<div class="block">Gets the wasLogHypInserted flag array.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getWasTheoremAppended()">getWasTheoremAppended</a></strong>()</code>
<div class="block">Gets the wasTheoremAppended flag.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getWasTheoremInserted()">getWasTheoremInserted</a></strong>()</code>
<div class="block">Gets the wasTheoremInserted flag.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#getWasTheoremUpdated()">getWasTheoremUpdated</a></strong>()</code>
<div class="block">Gets the wasTheoremUpdated flag.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#hashCode()">hashCode</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#initializeMustAppend()">initializeMustAppend</a></strong>()</code>
<div class="block">Initializes the mustAppend flag for the TheoremStmtGroup.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#queueDependentsForUpdate(java.util.Deque, java.util.List)">queueDependentsForUpdate</a></strong>(java.util.Deque&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;readyQueue,
                        java.util.List&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;waitingList)</code>
<div class="block">Requeues every MMT Theorem which uses this theorem.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#queueForUpdates(java.util.Queue, java.util.List)">queueForUpdates</a></strong>(java.util.Queue&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;readyQueue,
               java.util.List&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;waitingList)</code>
<div class="block">Queues the theorem into either the ready list or the waiting list.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#reverseStmtTblUpdates(java.util.Map)">reverseStmtTblUpdates</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl)</code>
<div class="block">Backs out the updates made into the Logical System.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#toString()">toString</a></strong>()</code>
<div class="block">Converts TheoremStmtGroup to String.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#updateLogicalSystem(mmj.lang.LogicalSystem, mmj.lang.Messages, mmj.tl.TlPreferences)">updateLogicalSystem</a></strong>(<a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                   <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                   <a href="../../mmj/tl/TlPreferences.html" title="class in mmj.tl">TlPreferences</a>&nbsp;tlPreferences)</code>
<div class="block">Adds or updates the LogicalSystem with the MMT Theorem and if the Logical
 System has a Proof Verifier it runs the Metamath Proof Verification
 algorithm.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/TheoremStmtGroup.html#validateTheoremSrcStmtProofLabels(mmj.lang.LogicalSystem, java.util.Map)">validateTheoremSrcStmtProofLabels</a></strong>(<a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                                 java.util.Map&lt;java.lang.String,<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;theoremStmtGroupTbl)</code>
<div class="block">Validates the labels used in the TheoremStmtGroup proof.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="SEQ">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>SEQ</h4>
<pre>public static final&nbsp;java.util.Comparator&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt; SEQ</pre>
<div class="block">SEQ sequences by TheoremStmtGroup.theorem.getSeq().</div>
</li>
</ul>
<a name="NBR_LOG_HYP_SEQ">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>NBR_LOG_HYP_SEQ</h4>
<pre>public static final&nbsp;java.util.Comparator&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt; NBR_LOG_HYP_SEQ</pre>
<div class="block">NBR_LOG_HYP_SEQ sequences by number of LogHyps and Seq.</div>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="TheoremStmtGroup(mmj.tl.MMTTheoremFile, mmj.lang.LogicalSystem, mmj.lang.Messages, mmj.tl.TlPreferences)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>TheoremStmtGroup</h4>
<pre>public&nbsp;TheoremStmtGroup(<a href="../../mmj/tl/MMTTheoremFile.html" title="class in mmj.tl">MMTTheoremFile</a>&nbsp;mmtTheoremFile,
                <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                <a href="../../mmj/tl/TlPreferences.html" title="class in mmj.tl">TlPreferences</a>&nbsp;tlPreferences)
                 throws <a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></pre>
<div class="block">Constructor for TheoremStmtGroup.
 <p>
 The constructor loads the input file into the TheoremStmtGroup and
 performs data validation of the input data.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mmtTheoremFile</code> - MMTTheoremFile to be read.</dd><dd><code>logicalSystem</code> - LogicalSystem object.</dd><dd><code>messages</code> - Messages object.</dd><dd><code>tlPreferences</code> - TlPreferences object.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></code> - is thrown if there are data errors in the
             input MMTTheoremFile.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="initializeMustAppend()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>initializeMustAppend</h4>
<pre>public&nbsp;void&nbsp;initializeMustAppend()</pre>
<div class="block">Initializes the mustAppend flag for the TheoremStmtGroup.
 <p>
 The initial (default) setting of mustAppend is false unless the theorem
 is new and has an incomplete proof.</div>
</li>
</ul>
<a name="validateTheoremSrcStmtProofLabels(mmj.lang.LogicalSystem, java.util.Map)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>validateTheoremSrcStmtProofLabels</h4>
<pre>public&nbsp;void&nbsp;validateTheoremSrcStmtProofLabels(<a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                                     java.util.Map&lt;java.lang.String,<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;theoremStmtGroupTbl)
                                       throws <a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></pre>
<div class="block">Validates the labels used in the TheoremStmtGroup proof.
 <p>
 During processing the highest sequence number referred to is updated,
 <p>
 Also, isProofIncomplete is set to true if a "?" is found in the proof.
 <p>
 And, two key lists about which theorems are used are updated:
 <code>theoremStmtGroupUsedList</code> and <code>usedByTheoremStmtGroupList</code>.
 These lists are the basis for determining the order in which theorems are
 loaded into the Logical System.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>logicalSystem</code> - LogicalSystem object.</dd><dd><code>theoremStmtGroupTbl</code> - the MMTTheoremSet Map containing the MMT
            Theorems in the set.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></code> - is thrown if there are data errors in the
             input MMTTheoremFile.</dd></dl>
</li>
</ul>
<a name="queueForUpdates(java.util.Queue, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>queueForUpdates</h4>
<pre>public&nbsp;void&nbsp;queueForUpdates(java.util.Queue&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;readyQueue,
                   java.util.List&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;waitingList)</pre>
<div class="block">Queues the theorem into either the ready list or the waiting list.
 <p>
 If the theorem's theoremStmtGroupUsedList is empty then it is ready to
 update because it doesn't refer to any other theorems in the
 MMTTheoremSet. Otherwise it goes into the waiting list. (When a theorem
 is stored into the LogicalSystem it is removed from the
 theoremStmtGroupUsedList of each theorem which refers to it.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>readyQueue</code> - queue of MMTTheorems ready for updating into the
            LogicalSystem.</dd><dd><code>waitingList</code> - list of MMTTheorems which are not yet ready to update
            into the LogicalSystem.</dd></dl>
</li>
</ul>
<a name="queueDependentsForUpdate(java.util.Deque, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>queueDependentsForUpdate</h4>
<pre>public&nbsp;void&nbsp;queueDependentsForUpdate(java.util.Deque&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;readyQueue,
                            java.util.List&lt;<a href="../../mmj/tl/TheoremStmtGroup.html" title="class in mmj.tl">TheoremStmtGroup</a>&gt;&nbsp;waitingList)
                              throws <a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></pre>
<div class="block">Requeues every MMT Theorem which uses this theorem.
 <p>
 When a theorem is stored into the LogicalSystem it is removed from the
 theoremStmtGroupUsedList of each theorem which refers to it. To determine
 which theorems need requeueing, the updated theorem's
 usedByTheoremStmtGroup list is read and each theorem in that list is
 requeued.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>readyQueue</code> - queue of MMTTheorems ready for updating into the
            LogicalSystem.</dd><dd><code>waitingList</code> - list of MMTTheorems which are not yet ready to update
            into the LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></code> - if a data error is discovered resulting
             from the theorem update.</dd></dl>
</li>
</ul>
<a name="updateLogicalSystem(mmj.lang.LogicalSystem, mmj.lang.Messages, mmj.tl.TlPreferences)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>updateLogicalSystem</h4>
<pre>public&nbsp;void&nbsp;updateLogicalSystem(<a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                       <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                       <a href="../../mmj/tl/TlPreferences.html" title="class in mmj.tl">TlPreferences</a>&nbsp;tlPreferences)
                         throws <a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a>,
                                <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Adds or updates the LogicalSystem with the MMT Theorem and if the Logical
 System has a Proof Verifier it runs the Metamath Proof Verification
 algorithm.
 <p>
 Note: a proof verification error does not trigger a
 TheoremLoaderException, which would thus halt the update of the entire
 MMTTheoremSet. Instead, any proof verification errors are stored in the
 Messages object for later display.
 <p>
 When a theorem is stored into the LogicalSystem it is removed from the
 theoremStmtGroupUsedList of each theorem which refers to it. To determine
 which theorems need requeueing, the updated theorem's
 usedByTheoremStmtGroup list is read and each theorem in that list is
 requeued.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>logicalSystem</code> - LogicalSystem object.</dd><dd><code>messages</code> - Messages object.</dd><dd><code>tlPreferences</code> - TlPreferences object.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></code> - if a data error is discovered.</dd>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if a data error is discovered.</dd></dl>
</li>
</ul>
<a name="reverseStmtTblUpdates(java.util.Map)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>reverseStmtTblUpdates</h4>
<pre>public&nbsp;void&nbsp;reverseStmtTblUpdates(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl)</pre>
<div class="block">Backs out the updates made into the Logical System.
 <p>
 If the theorem is new, it and its logical hypotheses are removed from the
 Logical System's statement table.
 <p>
 If the theorem was updated then the previous value of the theorem's proof
 and its $d restrictions are restored.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>stmtTbl</code> - the LogicalSystem object's stmtTbl.</dd></dl>
</li>
</ul>
<a name="getIsTheoremNew()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getIsTheoremNew</h4>
<pre>public&nbsp;boolean&nbsp;getIsTheoremNew()</pre>
<div class="block">Gets the isTheoremNew flag.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>isTheoremNew flag.</dd></dl>
</li>
</ul>
<a name="getTheoremLabel()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getTheoremLabel</h4>
<pre>public&nbsp;java.lang.String&nbsp;getTheoremLabel()</pre>
<div class="block">Gets the theorem label.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>theorem label.</dd></dl>
</li>
</ul>
<a name="getSourceFileName()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSourceFileName</h4>
<pre>public&nbsp;java.lang.String&nbsp;getSourceFileName()</pre>
<div class="block">Returns the MMTTheoremFile absolute pathname.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>MMTTheoremFile absolute pathname.</dd></dl>
</li>
</ul>
<a name="getWasTheoremUpdated()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getWasTheoremUpdated</h4>
<pre>public&nbsp;boolean&nbsp;getWasTheoremUpdated()</pre>
<div class="block">Gets the wasTheoremUpdated flag.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>wasTheoremUpdated flag.</dd></dl>
</li>
</ul>
<a name="getWasTheoremInserted()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getWasTheoremInserted</h4>
<pre>public&nbsp;boolean&nbsp;getWasTheoremInserted()</pre>
<div class="block">Gets the wasTheoremInserted flag.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>wasTheoremInserted flag.</dd></dl>
</li>
</ul>
<a name="getWasTheoremAppended()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getWasTheoremAppended</h4>
<pre>public&nbsp;boolean&nbsp;getWasTheoremAppended()</pre>
<div class="block">Gets the wasTheoremAppended flag.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>wasTheoremAppended flag.</dd></dl>
</li>
</ul>
<a name="getTheorem()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getTheorem</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;getTheorem()</pre>
<div class="block">Gets the Theorem object or null if the theorem is new and has not yet
 been stored in the Logical System.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Theorem object or null.</dd></dl>
</li>
</ul>
<a name="getWasLogHypInsertedArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getWasLogHypInsertedArray</h4>
<pre>public&nbsp;boolean[]&nbsp;getWasLogHypInsertedArray()</pre>
<div class="block">Gets the wasLogHypInserted flag array.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>wasLogHypInserted flag array.</dd></dl>
</li>
</ul>
<a name="getWasLogHypAppendedArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getWasLogHypAppendedArray</h4>
<pre>public&nbsp;boolean[]&nbsp;getWasLogHypAppendedArray()</pre>
<div class="block">Gets the wasLogHypAppended flag array.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>wasLogHypAppended flag array.</dd></dl>
</li>
</ul>
<a name="getLogHypArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLogHypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;getLogHypArray()</pre>
<div class="block">Gets the LogHyp array which may contain nulls if the Theorem is new and
 has not yet been stored in the Logical System.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>LogHyp array.</dd></dl>
</li>
</ul>
<a name="getInsertSectionNbr()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getInsertSectionNbr</h4>
<pre>public&nbsp;int&nbsp;getInsertSectionNbr()</pre>
<div class="block">Gets the BookManager insertSectionNbr for the theorem.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>BookManager insertSectionNbr for the theorem.</dd></dl>
</li>
</ul>
<a name="getAssignedLogHypSeq()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getAssignedLogHypSeq</h4>
<pre>public&nbsp;int[]&nbsp;getAssignedLogHypSeq()</pre>
<div class="block">Returns the assigned sequence number array for new Logical Hypotheses.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>assigned seq numbers of new Logical Hypotheses.</dd></dl>
</li>
</ul>
<a name="getAssignedTheoremSeq()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getAssignedTheoremSeq</h4>
<pre>public&nbsp;int&nbsp;getAssignedTheoremSeq()</pre>
<div class="block">Returns the assigned sequence number for a new Theorem.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>assigned seq numbers of a new Theorem.</dd></dl>
</li>
</ul>
<a name="toString()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>toString</h4>
<pre>public&nbsp;java.lang.String&nbsp;toString()</pre>
<div class="block">Converts TheoremStmtGroup to String.</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>toString</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
<dt><span class="strong">Returns:</span></dt><dd>returns TheoremStmtGroup string;</dd></dl>
</li>
</ul>
<a name="hashCode()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>hashCode</h4>
<pre>public&nbsp;int&nbsp;hashCode()</pre>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>hashCode</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
</dl>
</li>
</ul>
<a name="compareTo(java.lang.Object)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>compareTo</h4>
<pre>public&nbsp;int&nbsp;compareTo(java.lang.Object&nbsp;obj)</pre>
<div class="block">Compares TheoremStmtGroup object based on the label.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>obj</code> - TheoremStmtGroup object to compare to this TheoremStmtGroup</dd>
<dt><span class="strong">Returns:</span></dt><dd>returns negative, zero, or a positive int if this
         TheoremStmtGroup object is less than, equal to or greater than
         the input parameter obj.</dd></dl>
</li>
</ul>
<a name="equals(java.lang.Object)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>equals</h4>
<pre>public&nbsp;boolean&nbsp;equals(java.lang.Object&nbsp;obj)</pre>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code>equals</code>&nbsp;in class&nbsp;<code>java.lang.Object</code></dd>
</dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/tl/TlConstants.html" title="class in mmj.tl"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/tl/TheoremStmtGroup.html" target="_top">Frames</a></li>
<li><a href="TheoremStmtGroup.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
